int a <- 2;

int run()
pre {
	@ int a0 <- a
	@ a0 = 2
} body {
	inc(a, a);
	void inc(ref int b, ref int c) {
		b <- b + 1;
		writebool(a = b = c = 3);
		c <- c + 1;
		writebool(a = b = c = 4);
	}
} post {
	@ a = a0 + 2
}

void writebool(bool b) {
	if(b) write(1);
	else  write(0);
}
